Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar3/secret2005SLASHcime1.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> sortSu₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> sortSu₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> sortSu₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
sortSu₁(circ₂(sortSu₁(s), sortSu₁(id))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(id), sortSu₁(s))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
te₁(subst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> te₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

sortSu₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> sortSu₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> sortSu₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> sortSu₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
sortSu₁(circ₂(sortSu₁(s), sortSu₁(id))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(id), sortSu₁(s))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
te₁(subst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> te₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(t), sortSu₁(u)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> SORTSU₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> SORTSU₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))

The TRS R consists of the following rules:

sortSu₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> sortSu₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> sortSu₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> sortSu₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
sortSu₁(circ₂(sortSu₁(s), sortSu₁(id))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(id), sortSu₁(s))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
te₁(subst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> te₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(t), sortSu₁(u)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> SORTSU₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> SORTSU₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))

The TRS R consists of the following rules:

sortSu₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> sortSu₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> sortSu₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> sortSu₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
sortSu₁(circ₂(sortSu₁(s), sortSu₁(id))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(id), sortSu₁(s))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
te₁(subst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> te₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> SORTSU₁(circ₂(sortSu₁(t), sortSu₁(u)))
TE₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> TE₁(msubst₂(te₁(a), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))
SORTSU₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> SORTSU₁(circ₂(sortSu₁(s), sortSu₁(t)))

The TRS R consists of the following rules:

sortSu₁(circ₂(sortSu₁(cons₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> sortSu₁(cons₂(te₁(msubst₂(te₁(a), sortSu₁(t))), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(te₁(a), sortSu₁(t))))) -> sortSu₁(cons₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(cons₂(sop₁(lift), sortSu₁(t))))) -> sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))
sortSu₁(circ₂(sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))), sortSu₁(u))) -> sortSu₁(circ₂(sortSu₁(s), sortSu₁(circ₂(sortSu₁(t), sortSu₁(u)))))
sortSu₁(circ₂(sortSu₁(s), sortSu₁(id))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(id), sortSu₁(s))) -> sortSu₁(s)
sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(s))), sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(t))), sortSu₁(u))))) -> sortSu₁(circ₂(sortSu₁(cons₂(sop₁(lift), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t))))), sortSu₁(u)))
te₁(subst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(a), sortSu₁(id))) -> te₁(a)
te₁(msubst₂(te₁(msubst₂(te₁(a), sortSu₁(s))), sortSu₁(t))) -> te₁(msubst₂(te₁(a), sortSu₁(circ₂(sortSu₁(s), sortSu₁(t)))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.